(declare-fun f ((_ BitVec 8)) (_ BitVec 8))
(declare-fun f1 ((_ BitVec 8)) (_ BitVec 8))
(declare-fun a () (_ BitVec 8))
(declare-fun l1 () Bool)
(declare-fun l2 () Bool)
(assert (or (bvuge a (_ bv0 8)) (and false) (= (_ bv0 8) (f1 (bvxor a (_ bv1 8))))))
(assert (= l1 (= (_ bv0 8) (f1 (concat ((_ extract 7 1) a) (_ bv1 1))))))
(assert (= l2 (exists ((x (_ BitVec 8))) (or (= (f1 x) (f x)) (= x (bvadd a (_ bv1 8)))))))
(check-sat)
